
#use "hol.ml";;

#use "Rqe/make.ml";;

#use "tac.ml";;


   -------           ------
   q |- q            p |- p 
 -----------      -----------
 p /\ q |- q      p /\ q |- p 
-------------------------------
     p /\ q |- q /\ p

let p = `p:bool`
let q = `q:bool`
let init_p = INIT p
let init_q = INIT q
let and_l2 = ANDL2 p q init_q
let and_l1 = ANDL1 p q init_p
let andr = ANDR and_l2 and_l1

